From ea40cfb5dc04b037ab57731dbe74fbc9eed1270a Mon Sep 17 00:00:00 2001 From: DanieCuevas <43822444+DanielCuevas1208@users.noreply.github.com> Date: Mon, 3 Aug 2026 19:39:11 -0700 Subject: [PATCH] feat: extend gatework --- .github/workflows/ci.yml | 4 + CHANGELOG.md | 20 ++++ README.md | 128 ++++++++++++++++++------ fixtures/adder.golden.vcd | 2 +- fixtures/assert.golden.vcd | 2 +- fixtures/bus.golden.vcd | 89 ++++------------- fixtures/counter.golden.vcd | 2 +- fixtures/gates.golden.vcd | 2 +- fixtures/haddader.golden.vcd | 2 +- fixtures/hcounter.golden.vcd | 2 +- fixtures/libadder.golden.vcd | 2 +- fixtures/reg2.golden.vcd | 2 +- fixtures/register.golden.vcd | 2 +- fixtures/reset.golden.vcd | 2 +- fixtures/shared.golden.vcd | 2 +- fixtures/tristate.golden.vcd | 2 +- fixtures/unknown.golden.vcd | 2 +- fixtures/vector4.golden.vcd | 32 ++++++ fixtures/vector4.net | 17 ++++ gatework.cabal | 3 +- src/Gatework/Netlist.hs | 25 ++++- src/Gatework/Simulator.hs | 6 +- src/Gatework/VCD.hs | 84 +++++++++++++--- test/Spec.hs | 186 ++++++++++++++++++++++++++++++++++- 24 files changed, 491 insertions(+), 129 deletions(-) create mode 100644 fixtures/vector4.golden.vcd create mode 100644 fixtures/vector4.net diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index d9277e5..bad758e 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -84,6 +84,10 @@ jobs: run: cabal run gatework -- --netlist fixtures/bus.net --duration 3 --output /tmp/bus.vcd --set a=0101,b=1010 - name: Compare the bus demo with the golden file run: diff fixtures/bus.golden.vcd /tmp/bus.vcd + - name: Run the four-state vector demo + run: cabal run gatework -- --netlist fixtures/vector4.net --duration 2 --output /tmp/vector4.vcd --set a=0z01,b=01x0,en=1 --at 2 en=0 + - name: Compare the vector demo with the golden file + run: diff fixtures/vector4.golden.vcd /tmp/vector4.vcd - name: Run the shared bus demo run: cabal run gatework -- --netlist fixtures/shared.net --duration 8 --output /tmp/shared.vcd --set d0=0,e0=0,d1=1,e1=0 --at 2 e0=1 --at 4 e1=1 --at 6 e0=0 - name: Compare the shared bus demo with the golden file diff --git a/CHANGELOG.md b/CHANGELOG.md index acb85f5..578198e 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -5,6 +5,26 @@ All notable changes to Gatework appear in this file. The format follows the Keep a Changelog convention. This project uses semantic versioning. +## [0.12.0.0] - 2026-08-03 + +### Added + +- Render each bus as one multi-bit vector in the VCD header. +- Group bus values into one line in the VCD timeline. +- Use the standard VCD vector syntax for the values. +- Include unknown and floating values inside vector strings. +- Detect module-internal buses after flattening. +- Add a four-state vector demo fixture and a golden waveform. +- Add deterministic tests and a QuickCheck property for vector output. +- Extend the CI workflow to run the vector demo. + +### Changed + +- Group all bus bits under one VCD variable and identifier. +- Bump the package version to 0.12.0.0. +- Update the golden VCD files to the new version string. +- Update the bus golden file to the vector format. + ## [0.11.0.0] - 2026-08-03 ### Added diff --git a/README.md b/README.md index 826acc0..7e12b75 100644 --- a/README.md +++ b/README.md @@ -45,6 +45,9 @@ You can do these tasks: - Sample a whole bus into a register on one clock edge. - Check a single bus bit with an assertion. - Set a whole bus on the command line with one bit string. +- Read a whole bus as one multi-bit VCD vector. +- See unknown and floating values inside a VCD vector. +- Group module-internal buses into VCD vectors too. ## Architecture @@ -56,7 +59,7 @@ The project has five library modules. | `Gatework.Netlist` | Parses, validates, and flattens circuit files | | `Gatework.Report` | Renders the waveform as a text table | | `Gatework.Simulator` | Schedules signal changes | -| `Gatework.VCD` | Renders the waveform text | +| `Gatework.VCD` | Renders waveform text as signals and bus vectors | The data flow is: @@ -81,6 +84,7 @@ An asserted reset forces flip-flop outputs to their initial values. The recorder keeps the initial value and every later transition. The assertion checker compares declared expectations with the waveform. The VCD writer uses stable signal order and stable identifiers. +The VCD writer groups bus bits into multi-bit vectors. The report writer prints one row per change time. The repository layout is: @@ -504,6 +508,62 @@ The value 0101 means `a[0]=1`, `a[1]=0`, `a[2]=1`, and `a[3]=0`. Bit 0 is the least-significant bit. The value 1010 means `b[0]=0`, `b[1]=1`, `b[2]=0`, and `b[3]=1`. +## Multi-bit VCD vectors + +Run the four-state vector demo. + +```powershell +cabal run gatework -- --netlist fixtures/vector4.net --duration 2 --output vector4.vcd --set a=0z01,b=01x0,en=1 --at 2 en=0 +``` + +The command writes this output: + +```text +Wrote vector4.vcd +Signals: 15 +Duration: 2 time units +Assertions: 6 passed +``` + +The VCD header declares each bus as one vector. + +```text +$var wire 4 ! a[3:0] $end +$var wire 4 " b[3:0] $end +$var wire 1 # en $end +$var wire 4 $ x[3:0] $end +$var wire 2 % m[1:0] $end +``` + +The vector name shows the declared width and the bit range. +The timeline lists the whole bus value at each change time. + +```text +#0 +b0z01! +b01x0" +1# +b0xx1$ +bx1% +#2 +0# +bzz% +``` + +A vector value starts with the letter b. +The bit string lists the most-significant bit first. +The value `b0xx1` means x[3]=0, x[2]=x, x[1]=x, and x[0]=1. +Unknown and floating values appear inside the string. + +| Time | a[3:0] | b[3:0] | en | x[3:0] | m[1:0] | +| --- | --- | --- | --- | --- | --- | +| 0 | 0z01 | 01x0 | 1 | 0xx1 | x1 | +| 2 | 0z01 | 01x0 | 0 | 0xx1 | zz | + +At time 2 the enable goes low. +Both tri-state buffers float, so m reads zz. +The whole vector changes together on one line. + ## Sample output The file `fixtures/counter.golden.vcd` holds the complete counter waveform. @@ -617,41 +677,41 @@ x# ``` The file `fixtures/bus.golden.vcd` holds the bus demo waveform. -Its header maps each bus bit to one identifier: +Its header declares each bus as one vector: ```text -$var wire 1 ! a[0] $end -$var wire 1 " a[1] $end -$var wire 1 # a[2] $end -$var wire 1 $ a[3] $end +$var wire 4 ! a[3:0] $end +$var wire 4 " b[3:0] $end +$var wire 4 # x[3:0] $end +$var wire 4 $ n[3:0] $end +$var wire 4 % q[3:0] $end +$var wire 1 & clk $end +$var wire 2 ' hi[1:0] $end +$var wire 1 ( c0 $end ``` -Its timeline shows the settled values after the zero-delay transients: +Its timeline shows the settled vector values after the zero-delay transients: ```text #0 -1) -1* -1+ -1, -0- -0. -0/ -00 -18 +b0101! +b1010" +b1111# +b0000$ +b0000% +0& +b00' +0( +1( #1 -11 -12 -13 -14 -15 +b1111% +1& ``` -Here `)` is `x[0]`, `-` is `n[0]`, and `0` is `n[3]`. -The value `18` means `c0` is high. -The value `00` means `n[3]` is low. -The identifier `1` is `q[0]`. -The register outputs change together on the clock edge. +Here `!` is `a`, `#` is `x`, `$` is `n`, and `%` is `q`. +The value `b0101` means `a[3]=0`, `a[2]=1`, `a[1]=0`, and `a[0]=1`. +The value `b1111` means every bit of `x` is high. +The register output `q` changes together on the clock edge. ## Netlist format @@ -909,6 +969,7 @@ Deterministic tests also cover multi-driver resolution, scheduled driver changes Deterministic tests also cover module library loading, cross-library module references, duplicate module names, and library file validation. Deterministic tests also cover the report command, its header order, its counter table, and its golden output. Deterministic tests also cover whole-bus input values, their bit order, their error cases, scheduled whole-bus transitions, and their golden output. +Deterministic tests also cover VCD vectors, their header declarations, their grouped values, four-state vector values, and module-internal bus vectors. QuickCheck properties cover gate algebra, full adder correctness, scheduled input sampling, reset sampling, register width, and assertion soundness. QuickCheck properties also compare the hierarchical adder and counter with their flat versions. QuickCheck properties also cover the four-state model and the tri-state buffer truth table. @@ -917,6 +978,7 @@ QuickCheck properties also compare the shared bus with a per-time resolution mod QuickCheck properties also compare a library adder with its flat version. QuickCheck properties also compare the counter report with the simulated waveform. QuickCheck properties also compare whole-bus input values with per-bit reference values. +QuickCheck properties also compare every VCD vector value with the per-bit waveform. QuickCheck runs one hundred random cases for each property. The gate properties cover the complete truth table. @@ -935,16 +997,18 @@ The bus hierarchy property shows that a bus module matches its flat circuit. The shared-bus property compares each resolved wire value with a per-time model. The library adder property compares a library netlist with the flat adder. The counter report property compares each report cell with the simulated value. +The VCD vector property compares each vector value with the per-bit values at that time. ## Test status All tests pass on GHC 9.6.7 with Cabal 3.14 in the bundled container. The CI workflow runs the same checks on Ubuntu with GHC 9.6.6. -Golden tests compare the counter, register, reset, two-bit register, assertion, gate, hierarchical adder, library adder, hierarchical counter, adder, tri-state, undefined-state, bus, and shared-bus VCD text. +Golden tests compare the counter, register, reset, two-bit register, assertion, gate, hierarchical adder, library adder, hierarchical counter, adder, tri-state, undefined-state, bus, shared-bus, and four-state vector VCD text. The golden report test compares the counter report table with its golden file. CI runs every demo and compares its output with the golden file. CI runs the report demo and compares it with the report golden file. CI runs the bus demo with whole-bus input values. +CI runs the four-state vector demo and compares it with its golden file. CI confirms that a missing library file stops the run. ## Limitations @@ -962,7 +1026,9 @@ All gates use zero delay. Zero-delay gates can show combinational settling transients at clock edges and at time zero. Input changes apply only at scheduled times. They do not react to circuit state. -VCD output uses one module scope and one-bit signals. +VCD output uses one module scope. +A bus renders as one multi-bit vector. +A scalar signal renders as one bit. An asynchronous reset that releases on a clock edge is a race. The event order decides the result. A wide flip-flop uses one shared reset signal. @@ -974,7 +1040,8 @@ A library file cannot hold top-level declarations. The main netlist cannot shadow a library module. Two library files cannot define the same module. Modules flatten before simulation, so the VCD stays flat. -A bus expands into single-bit signals, so the VCD stays flat. +A bus expands into single-bit signals internally. +The VCD writer groups the bits into one vector again. A flip-flop bus output must have a `wire` or `output` declaration. A reference to a whole bus uses the declared width. An assertion addresses one bit, not a whole bus. @@ -987,6 +1054,7 @@ The report prints every signal in the stable signal order. ## Roadmap +Release 0.12.0.0 completed multi-bit values in the VCD timeline. Release 0.11.0.0 completed whole-bus input values on the command line. Release 0.10.0.0 completed the waveform report command. Release 0.9.0.0 completed module libraries. @@ -1000,7 +1068,7 @@ Release 0.2.0.0 completed scheduled input transitions. Remaining work: -1. Add multi-bit values in the VCD timeline. +1. Add configurable gate delays. ## License diff --git a/fixtures/adder.golden.vcd b/fixtures/adder.golden.vcd index 9219d11..c5892a9 100644 --- a/fixtures/adder.golden.vcd +++ b/fixtures/adder.golden.vcd @@ -2,7 +2,7 @@ $date generated deterministically by gatework $end $version - gatework 0.11.0.0 + gatework 0.12.0.0 $end $timescale 1ns $end $scope module gatework $end diff --git a/fixtures/assert.golden.vcd b/fixtures/assert.golden.vcd index f73e380..055ea1d 100644 --- a/fixtures/assert.golden.vcd +++ b/fixtures/assert.golden.vcd @@ -2,7 +2,7 @@ $date generated deterministically by gatework $end $version - gatework 0.11.0.0 + gatework 0.12.0.0 $end $comment assert y = 1 at 0 diff --git a/fixtures/bus.golden.vcd b/fixtures/bus.golden.vcd index ed44583..3ec57f0 100644 --- a/fixtures/bus.golden.vcd +++ b/fixtures/bus.golden.vcd @@ -2,7 +2,7 @@ $date generated deterministically by gatework $end $version - gatework 0.11.0.0 + gatework 0.12.0.0 $end $comment assert x[0] = 1 at 0 @@ -15,77 +15,30 @@ $comment $end $timescale 1ns $end $scope module gatework $end -$var wire 1 ! a[0] $end -$var wire 1 " a[1] $end -$var wire 1 # a[2] $end -$var wire 1 $ a[3] $end -$var wire 1 % b[0] $end -$var wire 1 & b[1] $end -$var wire 1 ' b[2] $end -$var wire 1 ( b[3] $end -$var wire 1 ) x[0] $end -$var wire 1 * x[1] $end -$var wire 1 + x[2] $end -$var wire 1 , x[3] $end -$var wire 1 - n[0] $end -$var wire 1 . n[1] $end -$var wire 1 / n[2] $end -$var wire 1 0 n[3] $end -$var wire 1 1 q[0] $end -$var wire 1 2 q[1] $end -$var wire 1 3 q[2] $end -$var wire 1 4 q[3] $end -$var wire 1 5 clk $end -$var wire 1 6 hi[0] $end -$var wire 1 7 hi[1] $end -$var wire 1 8 c0 $end +$var wire 4 ! a[3:0] $end +$var wire 4 " b[3:0] $end +$var wire 4 # x[3:0] $end +$var wire 4 $ n[3:0] $end +$var wire 4 % q[3:0] $end +$var wire 1 & clk $end +$var wire 2 ' hi[1:0] $end +$var wire 1 ( c0 $end $upscope $end $enddefinitions $end #0 -1! -0" -1# -0$ -0% -1& -0' +b0101! +b1010" +b1111# +b0000$ +b0000% +0& +b00' +0( 1( -0) -1) -0* -1* -0+ -1+ -0, -1, -0- -1- -0- -0. -1. -0. -0/ -1/ -0/ -00 -10 -00 -01 -02 -03 -04 -05 -06 -07 -08 -18 #1 -11 -12 -13 -14 -15 +b1111% +1& #2 -05 +0& #3 -15 +1& diff --git a/fixtures/counter.golden.vcd b/fixtures/counter.golden.vcd index 86ef1a4..2d7464f 100644 --- a/fixtures/counter.golden.vcd +++ b/fixtures/counter.golden.vcd @@ -2,7 +2,7 @@ $date generated deterministically by gatework $end $version - gatework 0.11.0.0 + gatework 0.12.0.0 $end $timescale 1ns $end $scope module gatework $end diff --git a/fixtures/gates.golden.vcd b/fixtures/gates.golden.vcd index a3c8098..209e2e4 100644 --- a/fixtures/gates.golden.vcd +++ b/fixtures/gates.golden.vcd @@ -2,7 +2,7 @@ $date generated deterministically by gatework $end $version - gatework 0.11.0.0 + gatework 0.12.0.0 $end $comment assert nand_out = 1 at 0 diff --git a/fixtures/haddader.golden.vcd b/fixtures/haddader.golden.vcd index e7240bd..cc1781b 100644 --- a/fixtures/haddader.golden.vcd +++ b/fixtures/haddader.golden.vcd @@ -2,7 +2,7 @@ $date generated deterministically by gatework $end $version - gatework 0.11.0.0 + gatework 0.12.0.0 $end $timescale 1ns $end $scope module gatework $end diff --git a/fixtures/hcounter.golden.vcd b/fixtures/hcounter.golden.vcd index 1f021f2..df1ff5a 100644 --- a/fixtures/hcounter.golden.vcd +++ b/fixtures/hcounter.golden.vcd @@ -2,7 +2,7 @@ $date generated deterministically by gatework $end $version - gatework 0.11.0.0 + gatework 0.12.0.0 $end $timescale 1ns $end $scope module gatework $end diff --git a/fixtures/libadder.golden.vcd b/fixtures/libadder.golden.vcd index e7240bd..cc1781b 100644 --- a/fixtures/libadder.golden.vcd +++ b/fixtures/libadder.golden.vcd @@ -2,7 +2,7 @@ $date generated deterministically by gatework $end $version - gatework 0.11.0.0 + gatework 0.12.0.0 $end $timescale 1ns $end $scope module gatework $end diff --git a/fixtures/reg2.golden.vcd b/fixtures/reg2.golden.vcd index c6e140d..e711fcf 100644 --- a/fixtures/reg2.golden.vcd +++ b/fixtures/reg2.golden.vcd @@ -2,7 +2,7 @@ $date generated deterministically by gatework $end $version - gatework 0.11.0.0 + gatework 0.12.0.0 $end $timescale 1ns $end $scope module gatework $end diff --git a/fixtures/register.golden.vcd b/fixtures/register.golden.vcd index de97888..536a2e6 100644 --- a/fixtures/register.golden.vcd +++ b/fixtures/register.golden.vcd @@ -2,7 +2,7 @@ $date generated deterministically by gatework $end $version - gatework 0.11.0.0 + gatework 0.12.0.0 $end $timescale 1ns $end $scope module gatework $end diff --git a/fixtures/reset.golden.vcd b/fixtures/reset.golden.vcd index 1d95ec7..1522df7 100644 --- a/fixtures/reset.golden.vcd +++ b/fixtures/reset.golden.vcd @@ -2,7 +2,7 @@ $date generated deterministically by gatework $end $version - gatework 0.11.0.0 + gatework 0.12.0.0 $end $timescale 1ns $end $scope module gatework $end diff --git a/fixtures/shared.golden.vcd b/fixtures/shared.golden.vcd index 555e6dd..c303915 100644 --- a/fixtures/shared.golden.vcd +++ b/fixtures/shared.golden.vcd @@ -2,7 +2,7 @@ $date generated deterministically by gatework $end $version - gatework 0.11.0.0 + gatework 0.12.0.0 $end $comment assert y = z at 0 diff --git a/fixtures/tristate.golden.vcd b/fixtures/tristate.golden.vcd index ec75d1d..897bb9a 100644 --- a/fixtures/tristate.golden.vcd +++ b/fixtures/tristate.golden.vcd @@ -2,7 +2,7 @@ $date generated deterministically by gatework $end $version - gatework 0.11.0.0 + gatework 0.12.0.0 $end $comment assert y = z at 0 diff --git a/fixtures/unknown.golden.vcd b/fixtures/unknown.golden.vcd index c089ace..e4e3a39 100644 --- a/fixtures/unknown.golden.vcd +++ b/fixtures/unknown.golden.vcd @@ -2,7 +2,7 @@ $date generated deterministically by gatework $end $version - gatework 0.11.0.0 + gatework 0.12.0.0 $end $comment assert q = x at 0 diff --git a/fixtures/vector4.golden.vcd b/fixtures/vector4.golden.vcd new file mode 100644 index 0000000..6ac4840 --- /dev/null +++ b/fixtures/vector4.golden.vcd @@ -0,0 +1,32 @@ +$date + generated deterministically by gatework +$end +$version + gatework 0.12.0.0 +$end +$comment + assert x[0] = 1 at 0 + assert x[1] = x at 0 + assert x[3] = 0 at 0 + assert m[0] = 1 at 0 + assert m[1] = x at 0 + assert m[0] = z at 2 +$end +$timescale 1ns $end +$scope module gatework $end +$var wire 4 ! a[3:0] $end +$var wire 4 " b[3:0] $end +$var wire 1 # en $end +$var wire 4 $ x[3:0] $end +$var wire 2 % m[1:0] $end +$upscope $end +$enddefinitions $end +#0 +b0z01! +b01x0" +1# +b0xx1$ +bx1% +#2 +0# +bzz% diff --git a/fixtures/vector4.net b/fixtures/vector4.net new file mode 100644 index 0000000..701d721 --- /dev/null +++ b/fixtures/vector4.net @@ -0,0 +1,17 @@ +# Four-state values inside multi-bit VCD vectors. +input a[4] +input b[4] +output x[4] +wire x[4] +input en +output m[2] +wire m[2] +gate XOR combine (a,b) -> x +gate TRIBUF drive0 (a[0],en) -> m[0] +gate TRIBUF drive1 (b[1],en) -> m[1] +assert x[0] = 1 at 0 +assert x[1] = x at 0 +assert x[3] = 0 at 0 +assert m[0] = 1 at 0 +assert m[1] = x at 0 +assert m[0] = z at 2 diff --git a/gatework.cabal b/gatework.cabal index 61da6af..f87b025 100644 --- a/gatework.cabal +++ b/gatework.cabal @@ -1,6 +1,6 @@ cabal-version: 3.0 name: gatework -version: 0.11.0.0 +version: 0.12.0.0 synopsis: Event-driven digital logic simulation in Haskell description: Gatework parses typed netlists, runs combinational gates and D @@ -14,6 +14,7 @@ description: The command-line tool loads libraries with the --library option. A waveform report command prints the signal values as a text table. The command-line tool also sets a whole bus with one bit string. + Buses render as multi-bit vectors in the VCD timeline. GTKWave and other waveform viewers can open the output. homepage: https://github.com/DanielCuevas1208/gatework bug-reports: https://github.com/DanielCuevas1208/gatework/issues diff --git a/src/Gatework/Netlist.hs b/src/Gatework/Netlist.hs index fb6aa29..fc802c9 100644 --- a/src/Gatework/Netlist.hs +++ b/src/Gatework/Netlist.hs @@ -129,7 +129,6 @@ data RawModule = RawModule data ParsedNetlist = ParsedNetlist { parsedModules :: Map String Module , parsedDeclarations :: [Declaration] - , parsedBusWidths :: Map String Int } emptyNetlist :: Netlist @@ -170,7 +169,7 @@ parseNetlistWithLibraries libraries source = do validateModulesWithSources sources modules widths <- topLevelWidths rawDeclarations declarations <- resolveTopLevel signatureModules widths rawDeclarations - netlist <- flattenParsed (ParsedNetlist modules declarations widths) + netlist <- flattenParsed (ParsedNetlist modules declarations) _ <- validateNetlist netlist pure netlist @@ -780,7 +779,7 @@ flattenParsed :: ParsedNetlist -> Either String Netlist flattenParsed parsed = do expanded <- concat <$> mapM (expandTop parsed) (parsedDeclarations parsed) let netlist = foldl' addDeclaration emptyNetlist expanded - pure netlist {netlistBusWidths = busWidthList (parsedBusWidths parsed)} + pure netlist {netlistBusWidths = busWidthList (inferBusWidths expanded)} expandTop :: ParsedNetlist -> Declaration -> Either String [Declaration] expandTop parsed declaration = case declaration of @@ -867,6 +866,26 @@ busWidthList :: Map String Int -> [(String, Int)] busWidthList widths = [(name, width) | (name, width) <- Map.toAscList widths, width > 1] +inferBusWidths :: [Declaration] -> Map String Int +inferBusWidths = foldl' addName Map.empty . concatMap declarationNames + where + declarationNames declaration = case declaration of + InputDeclaration name -> [name] + OutputDeclaration name -> [name] + WireDeclaration name -> [name] + FlipFlopDeclaration flipFlop -> dffOutput flipFlop + _ -> [] + addName widths name = case break (== '[') name of + (base, '[' : rest) + | not (null rest) + , last rest == ']' + , Just index <- readBracket (init rest) -> + Map.insertWith max base (index + 1) widths + _ -> widths + readBracket text = case reads text of + [(index, "")] -> Just index + _ -> Nothing + resolveInputAssignments :: Netlist -> [(String, String)] -> Either String [(String, Logic)] resolveInputAssignments netlist = fmap concat . mapM resolveOne where diff --git a/src/Gatework/Simulator.hs b/src/Gatework/Simulator.hs index 93ecb75..5cdff3a 100644 --- a/src/Gatework/Simulator.hs +++ b/src/Gatework/Simulator.hs @@ -19,6 +19,7 @@ import Gatework.Netlist data Simulation = Simulation { simulationDuration :: Time , simulationSignals :: [String] + , simulationBuses :: [(String, Int)] , simulationChanges :: Map String [(Time, Logic)] , simulationAssertions :: [Assertion] , simulationFailures :: [AssertionFailure] @@ -215,9 +216,10 @@ clockValue clock time = runQueue :: Netlist -> Map String [Gate] -> Map String [Gate] -> Time -> EventQueue -> State -> Changes -> Either String Simulation runQueue netlist byOutput byInput duration queue state changes = case Map.minViewWithKey queue of - Nothing -> Right (Simulation duration (netlistSignals netlist) changes [] []) + Nothing -> Right (Simulation duration (netlistSignals netlist) (netlistBusWidths netlist) changes [] []) Just ((time, pending), remaining) - | time > duration -> Right (Simulation duration (netlistSignals netlist) changes [] []) + | time > duration -> + Right (Simulation duration (netlistSignals netlist) (netlistBusWidths netlist) changes [] []) | otherwise -> do (nextQueue, nextState, nextChanges) <- settleAtTime netlist byOutput byInput duration time pending remaining state changes 0 diff --git a/src/Gatework/VCD.hs b/src/Gatework/VCD.hs index 30f412b..5a1ecad 100644 --- a/src/Gatework/VCD.hs +++ b/src/Gatework/VCD.hs @@ -3,6 +3,7 @@ module Gatework.VCD , writeVCD ) where +import Data.Char (isDigit) import Data.List (nub, sort) import qualified Data.Map.Strict as Map import qualified Paths_gatework (version) @@ -10,11 +11,16 @@ import Data.Version (showVersion) import Gatework.Logic import Gatework.Simulator +data VcdVariable + = VcdScalar String + | VcdVector String Int + deriving (Eq, Show) + renderVCD :: Simulation -> String renderVCD simulation = header ++ timeline where - signals = simulationSignals simulation - identifiers = zip signals (map identifierFor [0 ..]) + variables = vcdVariables simulation + identifiers = zip variables (map identifierFor [0 ..]) header = unlines ( [ "$date" , " generated deterministically by gatework" @@ -27,7 +33,7 @@ renderVCD simulation = header ++ timeline ++ [ "$timescale 1ns $end" , "$scope module gatework $end" ] - ++ ["$var wire 1 " ++ identifier ++ " " ++ signal ++ " $end" | (signal, identifier) <- identifiers] + ++ [renderDeclaration variable identifier | (variable, identifier) <- identifiers] ++ [ "$upscope $end" , "$enddefinitions $end" ] @@ -49,6 +55,13 @@ renderVCD simulation = header ++ timeline writeVCD :: FilePath -> Simulation -> IO () writeVCD path = writeFile path . renderVCD +renderDeclaration :: VcdVariable -> String -> String +renderDeclaration (VcdScalar signal) identifier = + "$var wire 1 " ++ identifier ++ " " ++ signal ++ " $end" +renderDeclaration (VcdVector base width) identifier = + "$var wire " ++ show width ++ " " ++ identifier ++ " " + ++ base ++ "[" ++ show (width - 1) ++ ":0] $end" + changeTimes :: Simulation -> [Time] changeTimes simulation = sort . nub $ [ time @@ -56,17 +69,66 @@ changeTimes simulation = sort . nub $ , (time, _) <- entries ] -renderTime :: Simulation -> [(String, String)] -> Time -> String +renderTime :: Simulation -> [(VcdVariable, String)] -> Time -> String renderTime simulation identifiers time = "#" ++ show time ++ "\n" - ++ concatMap (renderSignalChange simulation time) identifiers + ++ concatMap (renderVariableChange simulation time) identifiers -renderSignalChange :: Simulation -> Time -> (String, String) -> String -renderSignalChange simulation time (signal, identifier) = concat - [ [logicChar value] ++ identifier ++ "\n" - | (changeTime, value) <- signalChanges simulation signal - , changeTime == time - ] +renderVariableChange :: Simulation -> Time -> (VcdVariable, String) -> String +renderVariableChange simulation time (variable, identifier) = case variable of + VcdScalar signal -> + concat + [ [logicChar value] ++ identifier ++ "\n" + | (changeTime, value) <- signalChanges simulation signal + , changeTime == time + ] + VcdVector base width + | not (vectorChangedAt simulation base width time) -> "" + | otherwise -> + "b" ++ vectorValue simulation base width time ++ identifier ++ "\n" + +vectorChangedAt :: Simulation -> String -> Int -> Time -> Bool +vectorChangedAt simulation base width time = + any bitChangedAt [0 .. width - 1] + where + bitChangedAt index = + any ((== time) . fst) (signalChanges simulation (bitName base width index)) + +vectorValue :: Simulation -> String -> Int -> Time -> String +vectorValue simulation base width time = + [logicChar (bitValueAt simulation (bitName base width index) time) + | index <- [width - 1, width - 2 .. 0]] + +bitValueAt :: Simulation -> String -> Time -> Logic +bitValueAt simulation signal time = + case reverse [(changeTime, value) | (changeTime, value) <- signalChanges simulation signal, changeTime <= time] of + (_, value) : _ -> value + [] -> Low + +bitName :: String -> Int -> Int -> String +bitName base width index + | width <= 1 = base + | otherwise = base ++ "[" ++ show index ++ "]" + +vcdVariables :: Simulation -> [VcdVariable] +vcdVariables simulation = go (Map.fromList (simulationBuses simulation)) (simulationSignals simulation) + where + go _ [] = [] + go buses (signal : rest) = case parseBusBit signal of + Just (base, 0) + | Just width <- Map.lookup base buses + , take (width - 1) rest == [bitName base width index | index <- [1 .. width - 1]] -> + VcdVector base width : go (Map.delete base buses) (drop (width - 1) rest) + _ -> VcdScalar signal : go buses rest + +parseBusBit :: String -> Maybe (String, Int) +parseBusBit signal = case break (== '[') signal of + (base, '[' : rest) + | not (null rest) + , last rest == ']' + , all isDigit (init rest) -> + Just (base, read (init rest)) + _ -> Nothing identifierFor :: Int -> String identifierFor value = go value diff --git a/test/Spec.hs b/test/Spec.hs index fbbe4cd..e14fd27 100644 --- a/test/Spec.hs +++ b/test/Spec.hs @@ -6,7 +6,7 @@ import Data.Char (isSpace) import Data.Either (isLeft) import Data.List (elemIndex, find, foldl', isPrefixOf, nub, sort, sortOn) import qualified Data.Map.Strict as Map -import Gatework.Logic (GateType (..), Logic (..), evalGate, parseLogic) +import Gatework.Logic (GateType (..), Logic (..), evalGate, logicChar, parseLogic) import Gatework.Netlist ( Assertion (..) , Netlist (..) @@ -274,6 +274,11 @@ main = do , testWholeBusScalarValue , testWholeBusScheduledRegister , testWholeBusGoldenVCD + , testVCDVectorHeader + , testVCDVectorTimeline + , testVCDVectorFourState + , testVCDVectorModuleBus + , testGoldenVector4VCD ] properties <- forM [ ("AND is commutative", quickCheckResult propAndCommutative) @@ -320,6 +325,7 @@ main = do , ("library adder matches the flat adder", quickCheckResult (propLibraryAdderMatchesFlat adder libadder)) , ("counter report matches the waveform", quickCheckResult (propCounterReportMatchesWaveform counter)) , ("whole-bus values match per-bit values", quickCheckResult propWholeBusMatchesBitwise) + , ("VCD vectors match the per-bit waveform", quickCheckResult propVCDVectorMatchesBits) ] $ \(label, action) -> do result <- action @@ -1958,6 +1964,148 @@ testWholeBusGoldenVCD = do pure (renderVCD simulation) check "whole-bus VCD matches golden file" (actual == Right golden) +vectorInverter :: Either String Netlist +vectorInverter = parseNetlist (unlines + [ "input a[4]" + , "output y[4]" + , "wire y[4]" + , "gate NOT inv (a) -> y" + ]) + +testVCDVectorHeader :: IO Bool +testVCDVectorHeader = case vectorInverter of + Left _ -> check "VCD declares buses as multi-bit vectors" False + Right netlist -> case simulate netlist 0 of + Left _ -> check "VCD declares buses as multi-bit vectors" False + Right simulation -> + let text = renderVCD simulation + in check "VCD declares buses as multi-bit vectors" $ case parseVcd text of + Just vars -> + any (\var -> vcdVarName var == "a" && vcdVarWidth var == 4) vars + && any (\var -> vcdVarName var == "y" && vcdVarWidth var == 4) vars + && "$var wire 4 ! a[3:0] $end" `elem` lines text + && "$var wire 4 \" y[3:0] $end" `elem` lines text + Nothing -> False + +testVCDVectorTimeline :: IO Bool +testVCDVectorTimeline = case vectorInverter of + Left _ -> check "VCD timelines group bus values" False + Right netlist -> case + simulateWithInputs netlist + [("a[0]", High), ("a[1]", Low), ("a[2]", High), ("a[3]", Low)] 0 of + Left _ -> check "VCD timelines group bus values" False + Right simulation -> + let text = renderVCD simulation + in check "VCD timelines group bus values" $ case + (parseVcd text, parseVcdTimeline text) of + (Just vars, timeline) -> + vcdValueAt vars timeline "a" 0 == Just "0101" + && vcdValueAt vars timeline "y" 0 == Just "1010" + && "b0101!" `elem` lines text + && "b1010\"" `elem` lines text + (Nothing, _) -> False + +testVCDVectorFourState :: IO Bool +testVCDVectorFourState = do + source <- readFile "fixtures/vector4.net" + case parseNetlist source of + Left _ -> check "VCD vectors render x and z" False + Right netlist -> check "VCD vectors render x and z" $ case + resolveInputAssignments netlist [("a", "0z01"), ("b", "01x0"), ("en", "1")] of + Left _ -> False + Right overrides -> case + simulateWithScheduledInputs netlist overrides [(2, "en", Low)] 2 of + Left _ -> False + Right simulation -> + let text = renderVCD simulation + in case (parseVcd text, parseVcdTimeline text) of + (Just vars, timeline) -> + vcdValueAt vars timeline "x" 0 == Just "0xx1" + && vcdValueAt vars timeline "m" 0 == Just "x1" + && vcdValueAt vars timeline "m" 2 == Just "zz" + && "b0xx1$" `elem` lines text + && "bzz%" `elem` lines text + (Nothing, _) -> False + +testVCDVectorModuleBus :: IO Bool +testVCDVectorModuleBus = case parseNetlist (unlines + [ "module double (a[4]) -> (y[4])" + , " wire t[4]" + , " gate NOT first (a) -> t" + , " gate NOT second (t) -> y" + , "end" + , "input a[4]" + , "output y[4]" + , "wire y[4]" + , "instance double u (a) -> (y)" + ]) of + Left _ -> check "module buses render as vectors" False + Right netlist -> check "module buses render as vectors" $ case simulate netlist 0 of + Left _ -> False + Right simulation -> case parseVcd (renderVCD simulation) of + Just vars -> + any (\var -> vcdVarName var == "u.t" && vcdVarWidth var == 4) vars + Nothing -> False + +testGoldenVector4VCD :: IO Bool +testGoldenVector4VCD = do + source <- readFile "fixtures/vector4.net" + golden <- readFile "fixtures/vector4.golden.vcd" + let actual = do + netlist <- parseNetlist source + overrides <- resolveInputAssignments netlist [("a", "0z01"), ("b", "01x0"), ("en", "1")] + simulation <- simulateWithScheduledInputs netlist overrides [(2, "en", Low)] 2 + pure (renderVCD simulation) + check "vector4 VCD matches golden file" (actual == Right golden) + +data VcdVar = VcdVar + { vcdVarName :: String + , vcdVarId :: String + , vcdVarWidth :: Int + } + deriving (Eq, Show) + +parseVcd :: String -> Maybe [VcdVar] +parseVcd text = mapM parseVar declarations + where + declarations = [words line | line <- lines text, "$var" `isPrefixOf` line] + parseVar tokens = case tokens of + ["$var", "wire", widthText, identifier, name, "$end"] -> do + width <- readMaybe widthText + pure (VcdVar (baseOf name) identifier width) + _ -> Nothing + baseOf name = case break (== '[') name of + (base, _) -> base + +parseVcdTimeline :: String -> [(Time, [(String, String)])] +parseVcdTimeline text = reverse (go [] (lines text)) + where + go acc [] = acc + go acc (line : rest) + | '#' : timeText <- line + , Just time <- readMaybe timeText = go ((time, []) : acc) rest + | (identifier, value) <- parseValueLine line + , not (null identifier) + , (time, entries) : tailAcc <- acc = go ((time, (identifier, value) : entries) : tailAcc) rest + | otherwise = go acc rest + parseValueLine line = case line of + 'b' : rest + | not (null rest) -> + let (valueText, identifier) = span (`elem` "01xzXZ") rest + in (identifier, valueText) + 'B' : rest -> + let (valueText, identifier) = span (`elem` "01xzXZ") rest + in (identifier, valueText) + valueChar : identifier + | valueChar `elem` "01xzXZ" -> (identifier, [valueChar]) + _ -> ("", "") + +vcdValueAt :: [VcdVar] -> [(Time, [(String, String)])] -> String -> Time -> Maybe String +vcdValueAt vars timeline name time = do + var <- find ((== name) . vcdVarName) vars + (_, entries) <- find ((== time) . fst) timeline + lookup (vcdVarId var) entries + splitOn :: Char -> String -> [String] splitOn delimiter value = case break (== delimiter) value of (part, _ : rest) -> part : splitOn delimiter rest @@ -2284,6 +2432,42 @@ propWholeBusMatchesBitwise = property (renderVCD wholeSim == renderVCD bitSim) _ -> property False +propVCDVectorMatchesBits :: Property +propVCDVectorMatchesBits = + forAll (choose (0, 15)) $ \aValue -> + forAll (choose (0, 15)) $ \bValue -> + case busXorNetlist of + Left _ -> property False + Right netlist -> + case simulateWithInputs netlist (busInputs "a" aValue 4 ++ busInputs "b" bValue 4) 0 of + Left _ -> property False + Right simulation -> + let text = renderVCD simulation + in case parseVcd text of + Nothing -> property False + Just vars -> case parseVcdTimeline text of + [] -> property False + timeline -> + property (all (varMatches simulation timeline) vars) + where + varMatches simulation timeline var = + all (entryMatches simulation var) timeline + entryMatches simulation var (time, entries) = + case lookup (vcdVarId var) entries of + Nothing -> True + Just valueText -> valueText == expectedValue simulation var time + expectedValue simulation var time + | vcdVarWidth var == 1 = [logicChar (valueAt simulation (vcdVarName var) time)] + | otherwise = + [ logicChar (valueAt simulation (bitName (vcdVarName var) (vcdVarWidth var) index) time) + | index <- [vcdVarWidth var - 1, vcdVarWidth var - 2 .. 0] + ] + +bitName :: String -> Int -> Int -> String +bitName base width index + | width <= 1 = base + | otherwise = base ++ "[" ++ show index ++ "]" + propGatesFixture :: Netlist -> Property propGatesFixture netlist = forAll (elements [Low, High]) $ \a ->